Il a été introduit en 1962 par Martin Davis, Hilary Putnam, George Logemann et . C`est une extension de l`algorithme de Davis-Putnam, une procédure développée par Davis et Putnam en 1960 basée sur l`utilisation de la règle de résolution. Dans les premières publications sur ce sujet, L`a...